On-chip memories take up a major portion of the area of most modern high performance microprocessors available today. Due to the complexity of modern microprocessors, functions performed by on-chip memories, and other functional blocks, designs of microprocessors are complicated. Several models of a same microprocessor can be required spanning many levels of abstraction, beginning with a conceptual design addressing a desired functionality at a top level model and ending with a detailed model including information needed to construct the microprocessor on a silicon wafer.
The set of models representing the same microprocessor is called a design hierarchy. Typically, for a microprocessor design, different models can include a high level design described using a high level language suited for representing conceptual designs, a register transfer level (RTL) design described using a language suited for RTL descriptions, a gate-level design described using logic gates, and a circuit level design described using transistors, a physical design that is used to generate mask sets that are used in the fabrication process of laying out the microprocessor onto a silicon wafer or other substrates.
The process of designing successively detailed models for the same microprocessor is known as abstraction refinement.
As a part of the complete design, memories are also designed at each of the levels of abstraction, starting from the most abstract level model and ending at the most detailed level. The process of translation from one level to the next lower level is often manual. In such cases, design errors are common.
To address the problem of frequent errors, designers carefully check that each pair of successive levels of abstraction maintains functional equivalence. Therefore, verification of equivalence between two different descriptions of the memories and the ability to debug discrepancies between descriptions is of paramount importance for the semiconductor industry. To verify equivalence between two memory models, it is important that the user has the ability to provide correspondence between the storage elements (also known as bit-cells) that make up the two memory models.
When a memory design is taken from one level of abstraction to the next lower level of abstraction, certain aspects of the lower level design dictates the organization of the memory bit-cells in that level. For example, wafer size, power and speed of circuit operation considerations may require the organization of memory bit-cells at the transistor level model to be completely different from the organization of memory bit-cells at the RTL and/or the gate-level designs, because at those levels size, power and speed considerations are not very important. Therefore, due to the disparate memory organizations, the correspondence between the bit-cells of the RTL and transistor level memory models may be very complex and it may be time-consuming and error-prone to find the correspondence easily without the aid of a sophisticated automated mechanism.
Efficient automated solutions for identifying corresponding bit-cells of two memory models are, thus, required for efficient design and verification of memory models across the design hierarchy.
Currently, there are no methods that satisfactorily identify correspondence between bit-cells of two memory models. There are, however, techniques that find correspondence between storage elements, also referred to as “latches,” of two general purpose circuit models. Such methods that are effective for finding latch correspondence become extremely inefficient when applied to the problem of identifying bit-cell correspondence between two memory models.
One reason the latch correspondence methods are inefficient is that the methods for finding latch correspondence fail to address characteristics inherent in memory designs. Further, as one skilled in the art will readily appreciate, the large size of today's modern microprocessor memories make the latch correspondence techniques encounter what is known as the “state explosion” problem. The state explosion is a phenomenon in which the time and/or space required for solving a problem increases exponentially with the size of the problem. When known methods of finding latch correspondence are applied to find memory bit-cell correspondence, state explosion is encountered in the form of spending time and/or space that increases exponentially with respect to the number of bit-cells in the memory design—a number that in itself might be very large. For example, an “L2 cache” can have an on-chip memory present on almost every state-of-the-art microprocessor, and can have a million bit-cells. Therefore, all known methods of latch correspondence fail to perform bit-cell identification within an acceptable period of time and/or space on a relatively large memory design.
One prior art method teaches an iterative process that groups latches together into potential matches using the respective fan-in cones, fan-out cones and random simulation. The method fails to perform for memory circuits. First, all bit-cells in a given memory word have the same fan-in cone and so cannot be distinguished using fan-in analysis. Second, all bit-cells in the same memory column of a memory have the same fan-out cone and so cannot be distinguished using fan-out analysis. Third, being able to write into memory words using random simulation has no guarantee of success because, in the worst case, random simulations may never be able to write into a memory model using randomized input values. The prior art method does not guarantee finding the correspondence between the bit-cells of the two memory models. Thus, especially for memory circuits, the prior art is ineffective at finding correspondence of bit-cells between two memory descriptions.
Other prior art methods for latch correspondence use name-based information. As one skilled in the art will readily appreciate, however, there is little basis for matching memory bit-cells using the names of the bit-cells because, due to different hierarchy requirements at two different levels of abstraction, memory bit-cell names typically do not match between two different levels of memory models. Such name-based methods are, therefore, unable to find the correspondence between bit-cells of two memory models.
Other methods for finding latch correspondence employ functional fixed point iterations to refine the universe of all latches to find the correspondence. A problem with functional fixed point iterations is that the refinement process used is lengthy and inefficient because it explores all possible circuit behavior described in the circuit model. Due to the large size of modem memories these methods tend to experience state explosion and therefore, these methods are not effective for finding bit-cell correspondence for memory models. Therefore, when applied to modem memory designs with a large number of bit-cells, these methods take a disproportionately large amount of time (maybe years) to return a result.
What is needed is an apparatus and method for deriving correspondences between bit-cells of two different memory models of the same or different levels of abstraction that is efficient and can be effectively used in the design of a modem integrated circuit. There is a need for such an apparatus and method to enable a user to find bit-cell correspondence multiple times while moving a design from one level of abstraction to the next lower level of abstraction, from one design to a second design, or at the same level of abstraction.